$\forall$${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, ${\it da}_{1}$, ${\it da}_{2}$:$k$:Knd fp$\rightarrow$ Type.
\\[0ex]${\it ds}_{2}$ $\subseteq$ ${\it ds}_{1}$ $\Rightarrow$ ${\it da}_{2}$ $\subseteq$ ${\it da}_{1}$ $\Rightarrow$ ecl(${\it ds}_{2}$;${\it da}_{2}$) $\subseteq\rho$ ecl(${\it ds}_{1}$;${\it da}_{1}$)